Nuprl Lemma : eventtype_wf
11,40
postcript
pdf
E
:Type,
V
:(Id
Id
Type),
M
:(IdLnk
Id
Type),
loc
:(
E
Id),
k
:(
E
Knd),
e
:
E
.
eventtype(
k
;
loc
;
V
;
M
;
e
)
Type
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
eventtype(
k
;
loc
;
V
;
M
;
e
)
,
kindcase(
k
;
a
.
f
(
a
);
l
,
t
.
g
(
l
;
t
) )
,
P
Q
,
if
b
then
t
else
f
fi
,
islocal(
k
)
,
act(
k
)
,
lnk(
k
)
,
tag(
k
)
,
b
,
isl(
x
)
,
outr(
x
)
,
t
.1
,
outl(
x
)
,
t
.2
,
tt
,
ff
,
Knd
,
rcv(
l
,
tg
)
,
locl(
a
)
Lemmas
Knd
wf
,
Id
wf
,
IdLnk
wf
origin
E:Type, V:(Id
IdType), M:(IdLnkIdType), loc:(EId), k:(EKnd), e:E.
Type E:Type, V:(IdIdType), M:(IdLnkIdType), loc:(EId), k:(EKnd), e:E.
Type x:A. B(x) T
Q
b